Improve Safety Oracle
WIP!!!
方針
現在の Message DAG を元にagree側にとって"最悪"なケースをシミュレーションする
agree か disagree かわからないバリデータは disagree
あるバリデータが honest であるとき、それ以外の equivocation node は許容されている最大の数存在する
latest message が agree である validator のうち disagree に変わる可能性があるなら disagree になる
validator は得られる情報のうち最小の情報しか得られていない
equivocation は同時に$ t回起こる可能性がある。equivocation は他のノードにバレることはない。
finality 判断者を global state$ \sigma \in \Sigma_t と言うことにする
すべての latest message が agree である validator について disagree になるか調べる
Definitions
$ \mathrm{Disagreeing}(\sigma, p):= global で latest message が disagree or ? である validator の数。
$ \mathrm{Agreeing}(\sigma, p) := global で latest message が agree である validator の数。equivocation の可能性がある。
$ A_v := ある honest validator$ vの視点で latest message が agree であり、かつ、global の視点でその後で1度でも disagree していない validator の数。
$ A_v := \mathrm{Agreeing}(\mathrm{L_J^H}(\sigma, v), p) \cap \{v' \in V| ~\mathrm{Later\_Disagreeing}(\sigma, \mathrm{L_M^H}(\mathrm{L_J^H}(\sigma, v), v'), p) = \empty\}
nrryuya.icon > GlobalでequivocationしてるやつはOK?
Agreeingのやつはequivocation含まないので、上の定義だと、OKじゃない感じになる
MEMO: vがjustifyしているequivocationはどうする？
考え方
$ A-A_vのうち最大$ t個のノードが equivocation しているのに、validator v にとっては equivocation と認識できないと考える。
validator v にとっては、他の equivocation ノード以外の validators が意見を変えないときにおいて、最大で$ D + \min(A-A_v, t)の数のノードが disagree であると認識する。
nrryuya.icon >$ A_vからのequivocationは$ vにとって検知できる
つまり、$ A_v - D - \min(A - A_v, t) > 0であるならば、意見を変えない。
$ =のときは、agree の数と disagree の数が半々だけど、このとき決定的に disagree を採用するとする
もし、$ \le が成り立つならば、vはdisagreeになる可能性があるため、disagreeにする（最悪なケースを考える）
これを、変化が起きなくなるまで続けたときに、disagree の数が過半数を超えているならば finality は得られない可能性がある。逆にいえば、agree の数が過半数を超えていれば必ず finality が得られる。
より具体的なアルゴリズム
finality 検知
現在の Message DAG を元に、Latest Message Array を以下のように定義する。
$ \mathrm{LMA}[i]:= i番目のバリデータの latest message。agree = 0, disagree = 1.
例: $ \mathrm{LMA} = [0,0,0,1]
以下 LMA は global 視点のものとする。
また、各バリデータについて $ A_i を計算しておく
priority queue $ Pを用意して$ (A_i, i)を push する
また、Number of Agreeing Validators $ \mathrm{NAV}[i]:=A_i を定義する。
$ A_i := A_{v_i}
$ Pから最小の要素$ (A_i,i)を取り出して以下を調べる
$ \mathrm{LMA}[i] == 0 かどうか。違うなら continue
$ \mathrm{NAV}[i] == A_i かどうか。違うなら continue
nrryuya.icon > $ A_i が$ \mathrm{NAV}[i] より古い時の話
$ (A_i, i)が先程述べたように disagree になる可能性かどうかを調べる
disagree になるなら、$ A_iを agree と認識しているバリデータ$ j全てについて、
$ \mathrm{LMA}[j] = 1
$ Pに$ (A_j - 1, j)を push する。
$ \mathrm{NAV}[j] = A_j-1
disagree にならないなら、break
$ \mathrm{LMA}の要素のうち$ 0が過半数ならば、finality が得られる。
更新（新しい message を受け取ったとき）
影響のある範囲の$ \mathrm{LMA}を更新すれば良い
時間計算量
Message DAG を元に $ \mathrm{LMA}は構築されているものとする
ある新しい message $ mが届いた時、それを元に$ \mathrm{LMA}を更新する$ O(mが指す新しいメッセージ数)
$ Pの構築$ O(V^2)
$ Pを使う処理の最悪計算量$ O(V^2)
$ A_jが agree から disagree に変わる回数は高々$ O(V)回
デクリメントする回数が高々$ O(V)
挿入に$ O(\log V)
全体で$ O(V(V+\log V)) = O(V^2)
ただし、実際はそこまで多くないと考えられる
更新が止まる
$ V^2回デクリメントしなくちゃいけないケースはない（そのときはクリークなので）
こういうときはちゃんと計算量解析を行えばもっと少ないことが示せれる事が多い
空間計算量
$ O(\mathrm{Message DAG} の頂点+辺の数)